 package ch.epfl.lara.matcheck.ast;



  sealed abstract class Formula extends Trees
  final case class And(left: Formula, right: Formula) extends Formula  
  final case class Or(left: Formula, right: Formula) extends Formula  
  final case class Neg(f: Formula) extends Formula    
  // This is used only internally
  final case class Imply(left: Formula, right: Formula) extends Formula 
  final case class Equality(left: Formula, right: Formula) extends Formula
  final case class SetComprehension(binder: String, f: Formula) extends Formula

  abstract class Atom extends Formula 
  final case class Forall(bounded: String, form: Formula) extends Atom
  final case class SubsetEq(left: SetExpr, right: SetExpr) extends Atom 
  final case class EqSet(left: SetExpr, right:SetExpr) extends Atom
  final case class In(x: E, set: SetExpr) extends Atom
  
  
  abstract class E extends Atom {
    def makeName: String
  }
  final case class StringLit0(lit: String) extends E {
    override def makeName: String = lit 
  }
  final case object Tru extends E {
    override def makeName: String = "tru"
  }
  final case object Flse extends E {
    override def makeName: String = "flse"
  }

 
  abstract class Term extends E 
  final case class Function(name: String, elem: List[Term]) extends Term {
    override def makeName: String = "call_" + name 
  }
  abstract class CodeTerm extends Term
  final case class Element(name: String) extends CodeTerm {
    override def makeName: String = name
  }
  final case class Deref(obj: Element,field: CodeTerm) extends CodeTerm {
    override def makeName: String = obj.makeName + "__" + field.makeName
  }

  abstract class SetExpr extends Atom
  final case class Set(name: String) extends SetExpr 
  final case object EmptySet extends SetExpr
  final case class Union(left: SetExpr, right: SetExpr) extends SetExpr 
  final case class Intersection(left: SetExpr, right: SetExpr) extends SetExpr

  trait Atom0 extends Formula
  final case class Eq(left: E, right: E) extends Atom with Atom0
  final case class NotEq(left: E, right: E) extends Atom with Atom0
  final case class Less(left: E, right: E) extends Atom with Atom0
  final case class LessEq(left: E, right: E) extends Atom with Atom0


  // Linear Arithmetic Formulae
  abstract class Term0 extends Term with Atom0
  final case class Const(n: Int) extends Term0 {
    override def makeName: String = "const"
  }
  final case class Plus(left: Term, right: Term) extends Term0 {
    override def makeName: String = "plus"
  }
  final case class Minus(left: Term, right: Term) extends Term0 {
    override def makeName: String = "minus"
  }
  final case class Div(left: Term, right: Term) extends Term0 {
    override def makeName: String = "div"
  }
  final case class Prod(left: Term, right: Term) extends Term0 {
    override def makeName: String = "prod"
  }
  final case class Mod(left: Term, right: Term) extends Term0 {
    override def makeName: String = "mod"
  }
  // internally used
  final case class IntVar(x: String) extends Term0 {
    override def makeName: String = "intvar"
  }

  